『Simpliication of Girard's paradox』
Hurkens, Antonius J. C. “A simplification of Girard’s paradox”. Typed Lambda Calculi and Applications. Dezani-Ciancaglini, Mariangiola, Plotkin, Gordon編. Berlin, Heidelberg. Berlin, Heidelberg, Springer Berlin Heidelberg, 1995, p. 266–278.
1. どんなもの？
2. 先行研究と比べてどこがすごい？
Girardのオリジナルのパラドックスをより単純な形式で提示 3. 技術や手法のキモはどこ？
4. どうやって有効だと検証した？
数学的証明により、再帰型と汎用型を使って「矛盾する型」を構成 5. 議論はある？
6. 次に読むべき論文は？
Girard, J.-Y. (1989). Proofs and Types.
GirardによるSystem Fとそのメタ理論を詳述した古典的な教科書。Girardのパラドックスの詳細な導入や型理論の基礎的概念を網羅しており、本論文の出発点となる研究。 Coquand, T., & Huet, G. (1988). The Calculus of Constructions.
依存型システムを導入し、型と証明の統合的な取り扱いを提案した論文。ジラールのパラドックスに対抗する型理論の発展を理解するために重要。
Wadler, P. (1989). Theorems for free!.
System Fを用いて、型からプログラムの性質を導出する手法を提案した論文。型理論の実用的な側面や型安全性の応用を学ぶのに役立つ。
============================
table:訳
formalised 形式化された
Coquand コカン
proof 証明
normal form 正規形
analyse 解析する
behaviour 振る舞い
universe 宇宙（型の集合）
functions 関数
object 対象
well-founded 整礎
contradiction 矛盾
notation 記法
power set 冪集合
introduce 導入する
connected 結びついた
order 順序
sort ソート（型の分類）
rule 規則
variable 変数
natural number 自然数
step ステップ
proves 証明する
reduces 簡約する
disappears 消滅する
logic 論理
science 科学
editors 編集者
proceedings 議事録
equivalence relation 同値関係 System UはJean-Yves Girardが提唱した型理論の一つ
参考